 | ||||||
 |
 |
 |
 |
 |
 |
 |
 | ||||||
 |
 | |||||
|
|
|
|
| TUESDAY, June 8, 2004, 4:30 PM - 6:30 PM | Room: 6D | ||
|
TOPIC AREA: SYSTEM-LEVEL DESIGN AND VERIFICATION | ||
| SESSION 14 | |||
| Abstraction Techniques for Functional Verification | |||
| Chair: Vigyan Singhal - Jasper Design Automation, Mountain View, CA | |||
| Organizers: Karem A. Sakallah, Rajeev Ranjan | |||
| Abstraction techniques are essential for improving the capacity and performance of formal functional verification tools. The first paper combines bit-level SAT and word-level ILP solvers to verify both the control and datapath of RTL designs. The second paper performs automatic uninterpreted function abstraction of Verilog models to establish functional equivalence between an RTL design and its specification. The third paper enhances state-of-the-art abstraction refinement techniques by using two novel metrics. The last two papers describe case studies which demonstrate how real world designs can be effectively verified using formal methods. | |||
 14.1 |
An Efficient Finite Domain Constraint Solver for Circuits |
||
| Speaker(s): | Ganapathy Parthasarathy - Univ. of California, Santa Barbara, CA | ||
| Author(s): | Ganapathy Parthasarathy - Univ. of California, Santa Barbara, CA Madhu K. Iyer - Univ. of California, Santa Barbara, CA Kwang T. Cheng - Univ. of California, Santa Barbara, CA Li C. Wang - Univ. of California, Santa Barbara, CA | ||
| 14.2 | Automatic Abstraction and Verification of Verilog Models | ||
| Speaker(s): | Zaher S. Andraus - Univ. of Michigan, Ann Arbor, MI | ||
| Author(s): | Zaher S. Andraus - Univ. of Michigan, Ann Arbor, MI Karem A. Sakallah - Univ. of Michigan, Ann Arbor, MI | ||
| 14.3 | Abstraction Refinement by Controllability and Cooperativeness Analysis | ||
| Speaker(s): | Freddy Y.C. Mang - Synopsys, Inc., Mountain View, CA | ||
| Author(s): | Freddy Y. C. Mang - Synopsys, Inc., Mountain View, CA Pei-Hsin Ho - Synopsys, Inc., Portland, OR | ||
| 14.4s | Verifying a Gigabit Ethernet Switch Using SMV | ||
| Speaker(s): | Yuan Lu - Broadcom Corp., San Jose, CA | ||
| Author(s): | Yuan Lu - Broadcom Corp., San Jose, CA Mike Jorda - Broadcom Corp., San Jose, CA | ||
| 14.5s | A General Decomposition Strategy for Verifying Register Renaming | ||
| Speaker(s): | Mark D. Aagaard - Univ. of Waterloo, Waterloo, ON, Canada | ||
| Author(s): | Hazem I. Shehata - Univ. of Waterloo, Waterloo, ON, Canada Mark D. Aagaard - Univ. of Waterloo, Waterloo, ON, Canada | ||
 | |||